Inference at * 1 1 
Iof proof for Lemma connex iff trichot:



1. T : Type
2. R : TT
3. a, b:T. Dec(R(a,b))
4. x, y:T. R(x,y)  R(y,x)
5. a : T
6. b : T
  (R(a,b) & (R(b,a)))  (R(a,b) & R(b,a))  (R(b,a) & (R(a,b))) 

latex

 by ((((InstHyp [a;b] 4) 
CollapseTHENM (GenExRepD))) 
CollapseTHENA ((Auto_aux (first_nat 1:n
C) ((first_nat 1:n),(first_nat 4:n)) (first_tok :t) inil_term))) 

latex

C1: 

C1: 7. R(a,b)
C1:   (R(a,b) & (R(b,a)))  (R(a,b) & R(b,a))  (R(b,a) & (R(a,b)))
C2: 

C2: 7. R(b,a)
C2:   (R(a,b) & (R(b,a)))  (R(a,b) & R(b,a))  (R(b,a) & (R(a,b)))
C.

Definitions

t  T, P  Q, x:A. B(x)